\batchmode
\makeatletter
\def\input@path{{/Users/sergei.winitzki/Code/talks/ftt-fp/}}
\makeatother
\documentclass[english]{beamer}
\usepackage[T1]{fontenc}
\usepackage[latin9]{inputenc}
\setcounter{secnumdepth}{3}
\setcounter{tocdepth}{3}
\usepackage{babel}
\usepackage{amsmath}
\usepackage{graphicx}
\ifx\hypersetup\undefined
  \AtBeginDocument{%
    \hypersetup{unicode=true,pdfusetitle,
 bookmarks=true,bookmarksnumbered=false,bookmarksopen=false,
 breaklinks=false,pdfborder={0 0 1},backref=false,colorlinks=true}
  }
\else
  \hypersetup{unicode=true,pdfusetitle,
 bookmarks=true,bookmarksnumbered=false,bookmarksopen=false,
 breaklinks=false,pdfborder={0 0 1},backref=false,colorlinks=true}
\fi

\makeatletter

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% LyX specific LaTeX commands.
%% Because html converters don't know tabularnewline
\providecommand{\tabularnewline}{\\}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% Textclass specific LaTeX commands.
 % this default might be overridden by plain title style
 \newcommand\makebeamertitle{\frame{\maketitle}}%
 % (ERT) argument for the TOC
 \AtBeginDocument{%
   \let\origtableofcontents=\tableofcontents
   \def\tableofcontents{\@ifnextchar[{\origtableofcontents}{\gobbletableofcontents}}
   \def\gobbletableofcontents#1{\origtableofcontents}
 }
 \newenvironment{lyxcode}
   {\par\begin{list}{}{
     \setlength{\rightmargin}{\leftmargin}
     \setlength{\listparindent}{0pt}% needed for AMS classes
     \raggedright
     \setlength{\itemsep}{0pt}
     \setlength{\parsep}{0pt}
     \normalfont\ttfamily}%
    \def\{{\char`\{}
    \def\}{\char`\}}
    \def\textasciitilde{\char`\~}
    \item[]}
   {\end{list}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% User specified LaTeX commands.
\usetheme[secheader]{Boadilla}
\usecolortheme{seahorse}
\title[Introduction to Curry-Howard]{Introduction to the Curry-Howard
correspondence}
\subtitle{The logic of types in functional programming languages}
\author{Sergei Winitzki}
\date{February 17, 2018}
\institute[ABTB]{Academy by the Bay}
\setbeamertemplate{headline}{} % disable headline at top
\setbeamertemplate{navigation symbols}{}

\makeatother

\begin{document}
\frame{\titlepage}
\begin{frame}{Type constructions in functional programming}


\framesubtitle{The common ground between OCaml, Haskell, Scala, Rust, and other
languages}

Type constructions common in FP languages:
\begin{itemize}
\item Tuple (``product'') type: $\text{Int}\times\text{String}$
\item Function type: $\text{Int}\Rightarrow\text{String}$
\item Disjunction (``sum'') type: $\text{Int}+\text{String}$
\item Unit type (``empty tuple''): $1$
\item Type parameters: $\text{List}^{T}$
\end{itemize}
Up to differences in syntax, the FP languages share all these features
\end{frame}

\begin{frame}{Type constructions: Scala syntax}

\begin{itemize}
\item Tuple type: \texttt{\textcolor{blue}{\footnotesize{}(Int, String)}}{\footnotesize \par}
\begin{itemize}
\item Create: \texttt{\textcolor{blue}{\footnotesize{}val pair:\ (Int,
String) = (123, \textquotedbl{}abc\textquotedbl{})}} 
\item Use: \texttt{\textcolor{blue}{\footnotesize{}val y:\ String = pair.\_2}}{\footnotesize \par}
\end{itemize}
\item Function type: \texttt{\textcolor{blue}{\footnotesize{}Int $\Rightarrow$
String}}{\footnotesize \par}
\begin{itemize}
\item Create: \texttt{\textcolor{blue}{\footnotesize{}def f:\ (Int $\Rightarrow$
String) = x $\Rightarrow$ \textquotedbl{}Value is \textquotedbl{}
+ x.toString}} 
\item Use: \texttt{\textcolor{blue}{\footnotesize{}val y:\ String = f(123)}}{\footnotesize \par}
\end{itemize}
\item Disjunction type: \texttt{\textcolor{blue}{\footnotesize{}Either{[}Int,
String{]}}} defined in standard library
\begin{itemize}
\item Create:\\
 \texttt{\textcolor{blue}{\footnotesize{}\ val x:\ Either{[}Int,
String{]} = Left(123)}}~\\
\texttt{\textcolor{blue}{\footnotesize{} val y:\ Either{[}Int, String{]}
= Right(\textquotedbl{}abc\textquotedbl{})}}{\footnotesize \par}
\item Use: \texttt{\textcolor{blue}{\footnotesize{}val z:\ Boolean = x
match \{}}~\\
\texttt{\textcolor{blue}{\footnotesize{} case Left(i) $\Rightarrow$
i > 0}}~\\
\texttt{\textcolor{blue}{\footnotesize{} case Right(\_) $\Rightarrow$
false}}~\\
\texttt{\textcolor{blue}{\footnotesize{}\}}}{\footnotesize \par}
\end{itemize}
\item Unit type: \texttt{\textcolor{blue}{\footnotesize{}Unit}}{\footnotesize \par}
\begin{itemize}
\item Create: \texttt{\textcolor{blue}{\footnotesize{}val x:\ Unit = ()}}{\footnotesize \par}
\end{itemize}
\end{itemize}
\end{frame}

\begin{frame}{Type constructions: OCaml syntax}

\begin{itemize}
\item Tuple type: \texttt{\textcolor{blue}{\footnotesize{}int {*} string}}{\footnotesize \par}
\begin{itemize}
\item Create: \texttt{\textcolor{blue}{\footnotesize{}let pair:\ int {*}
string = (123, \textquotedbl{}abc\textquotedbl{})}} 
\item Use: \texttt{\textcolor{blue}{\footnotesize{}let y:\ string = snd
pair}}{\footnotesize \par}
\end{itemize}
\item Function type: \texttt{\textcolor{blue}{\footnotesize{}int -> string}}{\footnotesize \par}
\begin{itemize}
\item Create: \texttt{\textcolor{blue}{\footnotesize{}let f:\ int -> string
=}}~\\
\texttt{\textcolor{blue}{\footnotesize{} fun x -> Printf.sprintf \textquotedbl{}Value
is \%d\textquotedbl{} x}} 
\item Use: \texttt{\textcolor{blue}{\footnotesize{}let y:\ string = f 123}}{\footnotesize \par}
\end{itemize}
\item Disjunction type: \texttt{\textcolor{blue}{\footnotesize{}type e =
Left of int | Right of string}}{\footnotesize \par}
\begin{itemize}
\item Create:\\
 \texttt{\textcolor{blue}{\footnotesize{}\ let x:\ e = Left 123}}~\\
\texttt{\textcolor{blue}{\footnotesize{} let y:\ e = Right \textquotedbl{}abc\textquotedbl{}}}{\footnotesize \par}
\item Use: \texttt{\textcolor{blue}{\footnotesize{}let z:\ bool = match
x with}}~\\
\texttt{\textcolor{blue}{\footnotesize{} Left i -> i > 0}}~\\
\texttt{\textcolor{blue}{\footnotesize{} Right \_ -> false}}~\\
{\footnotesize \par}
\end{itemize}
\item Unit type: \texttt{\textcolor{blue}{\footnotesize{}unit}}{\footnotesize \par}
\begin{itemize}
\item Create: \texttt{\textcolor{blue}{\footnotesize{}let x:\ unit = ()}}{\footnotesize \par}
\end{itemize}
\end{itemize}
\end{frame}

\begin{frame}{Type constructions: Haskell syntax}

\begin{itemize}
\item Tuple type: \texttt{\textcolor{blue}{\footnotesize{}(Int, String)}}{\footnotesize \par}
\begin{itemize}
\item Create: \texttt{\textcolor{blue}{\footnotesize{}pair = (123, \textquotedbl{}abc\textquotedbl{})}} 
\item Use: \texttt{\textcolor{blue}{\footnotesize{}(\_, y) = pair}}{\footnotesize \par}
\end{itemize}
\item Function type: \texttt{\textcolor{blue}{\footnotesize{}Int -> String}}{\footnotesize \par}
\begin{itemize}
\item Create: \texttt{\textcolor{blue}{\footnotesize{}f = \textbackslash{}x
-> \textquotedbl{}Value is \textquotedbl{} ++ show x}} 
\item Use: \texttt{\textcolor{blue}{\footnotesize{}y = f 123}}{\footnotesize \par}
\end{itemize}
\item Disjunction type: \texttt{\textcolor{blue}{\footnotesize{}data E =
Left Int | Right String}}{\footnotesize \par}
\begin{itemize}
\item Create:\\
\  \texttt{\textcolor{blue}{\footnotesize{}x = Left 123}}~\\
\texttt{\textcolor{blue}{\footnotesize{} y = Right \textquotedbl{}abc\textquotedbl{}}}{\footnotesize \par}
\item Use: \texttt{\textcolor{blue}{\footnotesize{}z = case x of}}~\\
\texttt{\textcolor{blue}{\footnotesize{} Left i -> i > 0}}~\\
\texttt{\textcolor{blue}{\footnotesize{} Right \_ -> false}}~\\
{\footnotesize \par}
\end{itemize}
\item Unit type: \texttt{\textcolor{blue}{\footnotesize{}Unit}}{\footnotesize \par}
\begin{itemize}
\item Create: \texttt{\textcolor{blue}{\footnotesize{}x = ()}}{\footnotesize \par}
\end{itemize}
\end{itemize}
\end{frame}

\begin{frame}{From types to propositions}

The code \texttt{\textcolor{blue}{\footnotesize{}val x:\ T =}} ...
shows that \emph{we can compute a value} of type \texttt{\textcolor{blue}{\footnotesize{}T}}
as part of our program expression
\begin{itemize}
\item Let's denote this \emph{proposition} by ${\cal CH}(T)$ \textendash{}
``$\mathcal{C}$ode $\mathcal{H}$as a value of type \texttt{\textcolor{blue}{\footnotesize{}T}}''
\item Correspondence between types and propositions, for a given program:
\end{itemize}
\begin{center}
\begin{tabular}{|c|c|c|}
\hline 
\textbf{Type} &
\textbf{Proposition} &
\textbf{Short notation}\tabularnewline
\hline 
\hline 
\texttt{\textcolor{blue}{\footnotesize{}T}} &
${\cal CH}(T)$ &
$T$\tabularnewline
\hline 
\texttt{\textcolor{blue}{\footnotesize{}(A, B)}} &
${\cal CH}(A)$ \emph{and} ${\cal CH}(B)$ &
$A\wedge B$; $A\times B$\tabularnewline
\hline 
\texttt{\textcolor{blue}{\footnotesize{}Either{[}A, B{]}}} &
${\cal CH}(A)$ \emph{or} ${\cal CH}(B)$ &
$A\vee B$; $A+B$\tabularnewline
\hline 
\texttt{\textcolor{blue}{\footnotesize{}A $\Rightarrow$ B}} &
${\cal CH}(A)$ \emph{implies} ${\cal CH}(B)$ &
$A\Rightarrow B$\tabularnewline
\hline 
\texttt{\textcolor{blue}{\footnotesize{}Unit}} &
\emph{True} &
1\tabularnewline
\hline 
\end{tabular}
\par\end{center}
\begin{itemize}
\item Type parameter \texttt{\textcolor{blue}{\footnotesize{}{[}T{]}}} in
a function type means $\forall T$
\item Example: \texttt{\textcolor{blue}{\footnotesize{}def dupl{[}A{]}:\ A
$\Rightarrow$ (A, A)}}. The type of this function, $A\Rightarrow A\times A$,
corresponds to the theorem $\forall A:A\Rightarrow A\wedge A$
\end{itemize}
\end{frame}

\begin{frame}{Translating language constructions into the logic I}


\framesubtitle{How to represent logical relationships between ${\cal CH}(...)$
propositions?}

Code expressions create\,\emph{logical relationships} between propositions
${\cal CH}(...)$
\begin{itemize}
\item ``Logical relationships'' = what will be true if something given
is true
\item The elementary proof task is represented by a \textbf{sequent}
\begin{itemize}
\item Notation: $A,B,C\vdash G$; the \textbf{premises} are $A,B,C$ and
the \textbf{goal} is G
\end{itemize}
\item Proofs are achieved via axioms and derivation rules
\begin{itemize}
\item Axioms: such and such sequents are already true
\item Derivation rules: this sequent is true if such and such sequents are
true
\end{itemize}
\item To make connection with logic, represent code fragments as \textbf{sequents}
\item \textcolor{blue}{$A,B\vdash C$} represents an \emph{expression} of
type \texttt{\textcolor{blue}{\footnotesize{}C}} that uses \texttt{\textcolor{blue}{\footnotesize{}x:\ A}}
and \texttt{\textcolor{blue}{\footnotesize{}y:\ B}}{\footnotesize \par}
\item Examples in Scala:
\begin{itemize}
\item \texttt{\textcolor{blue}{\footnotesize{}(x:\ Int).toString + \textquotedbl{}abc\textquotedbl{}}}
is an expression of type \texttt{\textcolor{blue}{\footnotesize{}String}}
that uses an \texttt{\textcolor{blue}{\footnotesize{}x:\ Int}} and
is represented by the sequent $\text{Int}\vdash\text{String}$
\item \texttt{\textcolor{blue}{\footnotesize{}(x:\ Int) $\Rightarrow$
x.toString + \textquotedbl{}abc\textquotedbl{}}} is an expression
of type \texttt{\textcolor{blue}{\footnotesize{}Int $\Rightarrow$
String}} and is represented by the sequent $\emptyset\vdash\text{Int}\Rightarrow\text{String}$
\end{itemize}
\item Sequents only describe the \emph{types} of expressions and their parts
\end{itemize}
\end{frame}

\begin{frame}{Translating language constructions into the logic II}


\framesubtitle{What are the derivation rules for the logic of types?}

Write all the constructions in FP languages as sequents
\begin{itemize}
\item This will give all the derivation rules for the logic of types
\begin{itemize}
\item Each type construction has an expression for creating it and an expression
for using it
\end{itemize}
\item Tuple type $A\times B$
\begin{itemize}
\item Create: $A,B\vdash A\times B$ 
\item Use: $A\times B\vdash A$ and also $A\times B\vdash B$
\end{itemize}
\item Function type $A\Rightarrow B$
\begin{itemize}
\item Create: if we have $A\vdash B$ then we will have $\emptyset\vdash A\Rightarrow B$ 
\item Use: $A\Rightarrow B,A\vdash B$
\end{itemize}
\item Disjunction type $A+B$
\begin{itemize}
\item Create: $A\vdash A+B$ and also $B\vdash A+B$
\item Use: $A+B,A\Rightarrow C,B\Rightarrow C\vdash C$
\end{itemize}
\item Unit type $1$
\begin{itemize}
\item Create: $\emptyset\vdash1$
\end{itemize}
\end{itemize}
\end{frame}

\begin{frame}{Translating language constructions into the logic III}


\framesubtitle{Additional rules for the logic of types}

In addition to constructions that use types, we have ``trivial''
constructions:
\begin{itemize}
\item a single, unmodified value of type $A$ is a valid expression of type
$A$
\begin{itemize}
\item For any $A$ we have the sequent $A\vdash A$
\end{itemize}
\item if a value can be computed using some given data, it can also be computed
if given\,\emph{additional} data
\begin{itemize}
\item If we have $A,...,C\vdash G$ then also $A,...,C,D\vdash G$ for any
$D$
\item For brevity, we denote by $\Gamma$ a sequence of arbitrary premises
\end{itemize}
\item the order in which data is given does not matter, we can still compute
all the same things given the same premises in different order
\begin{itemize}
\item If we have $\Gamma,A,B\vdash G$ then we also have $\Gamma,B,A\vdash G$
\end{itemize}
\end{itemize}
Syntax conventions:
\begin{itemize}
\item the implication operation associates \emph{to the right}
\begin{itemize}
\item $A\Rightarrow B\Rightarrow C$ means $A\Rightarrow\left(B\Rightarrow C\right)$
\end{itemize}
\item precedence order: implication, disjunction, conjunction
\begin{itemize}
\item $A+B\times C\Rightarrow D$ means $\left(A+\left(B\times C\right)\right)\Rightarrow D$
\end{itemize}
\end{itemize}
Quantifiers: implicitly, all our type variables are universally quantified
\begin{itemize}
\item When we write $A\Rightarrow B\Rightarrow A$, we mean $\forall A:\forall B:A\Rightarrow B\Rightarrow A$
\end{itemize}
\end{frame}

\begin{frame}{The logic of types I}

Now we have all the axioms and the derivation rules of the logic of
types.
\begin{itemize}
\item What theorems can we derive in this logic?
\item Example: $A\Rightarrow B\Rightarrow A$
\begin{itemize}
\item Start with an axiom $A\vdash A$; add an unused extra premise $B$:
$A,B\vdash A$
\item Use the ``create function'' rule with $B$ and $A$, get $A\vdash B\Rightarrow A$
\item Use the ``create function'' rule with $A$ and $B\Rightarrow A$,
get the final sequent $\emptyset\vdash A\Rightarrow B\Rightarrow A$
showing that $A\Rightarrow B\Rightarrow A$ is a \textbf{theorem}
since it is derived from no premises
\end{itemize}
\item What code does this describe?
\begin{itemize}
\item The axiom $A\vdash A$ represents the expression $x^{A}$ where $x$
is of type $A$
\item The unused premise $B$ corresponds to unused variable $y^{B}$ of
type $B$
\item The ``create function'' rule gives the function $y^{B}\Rightarrow x^{A}$
\item The second ``create function'' rule gives $x^{A}\Rightarrow\left(y^{B}\Rightarrow x\right)$
\item Scala code: \texttt{\textcolor{blue}{\footnotesize{}def f{[}A, B{]}:\ A
$\Rightarrow$ B $\Rightarrow$ A = (x:\ A) $\Rightarrow$ (y:\ B)
$\Rightarrow$ x}}{\footnotesize \par}
\end{itemize}
\item Any code expression's type can be translated into a sequent
\item A proof of a theorem directly guides us in writing code for that type
\end{itemize}
\end{frame}

\begin{frame}{Correspondence between programs and proofs}

\begin{itemize}
\item By construction, any theorem can be implemented in code
\end{itemize}
\begin{center}
\begin{tabular}{|c|c|}
\hline 
\textbf{Proposition} &
\textbf{Code}\tabularnewline
\hline 
\hline 
$\forall A:A\Rightarrow A$ &
\texttt{\textcolor{blue}{\footnotesize{}def identity{[}A{]}(x:\ A):\ A
= x}}\tabularnewline
\hline 
$\forall A:A\Rightarrow1$ &
\texttt{\textcolor{blue}{\footnotesize{}def toUnit{[}A{]}(x:\ A): Unit
= ()}}\tabularnewline
\hline 
$\forall A\forall B:A\Rightarrow A+B$ &
\texttt{\textcolor{blue}{\footnotesize{}def inLeft{[}A,B{]}(x:A):\ Either{[}A,B{]}
= Left(x)}}\tabularnewline
\hline 
$\forall A\forall B:A\times B\Rightarrow A$ &
\texttt{\textcolor{blue}{\footnotesize{}def first{[}A,B{]}(p:\ (A,B)):\ A
= p.\_1}}\tabularnewline
\hline 
$\forall A\forall B:A\Rightarrow B\Rightarrow A$ &
\texttt{\textcolor{blue}{\footnotesize{}def const{[}A,B{]}(x:\ A):\ B$\Rightarrow$A
= (y:B)$\Rightarrow$x}}\tabularnewline
\hline 
\end{tabular}
\par\end{center}
\begin{itemize}
\item Also, non-theorems \emph{cannot be implemented} in code 
\begin{itemize}
\item Examples of non-theorems:\\
 $\forall A:1\Rightarrow A$; \  \  $\quad\forall A\forall B:A+B\Rightarrow A$;
\\
$\forall A\forall B:A\Rightarrow A\times B$; \  $\quad\forall A\forall B:(A\Rightarrow B)\Rightarrow A$
\end{itemize}
\item Given a type's formula, can we implement it in code? Not obvious.
\begin{itemize}
\item Example: $\forall A\forall B:((((A\Rightarrow B)\Rightarrow A)\Rightarrow A)\Rightarrow B)\Rightarrow B$
\begin{itemize}
\item Can we write a function with this type? Can we prove this formula?
\end{itemize}
\end{itemize}
\end{itemize}
\end{frame}

\begin{frame}{The logic of types II}


\framesubtitle{What kind of logic is this? What do mathematicians call this logic?}

This is called ``intuitionistic propositional logic'', IPL (also
``constructive'')
\begin{itemize}
\item This is a ``nonclassical'' logic because it is different from Boolean
logic
\item Disjunction works very differently from Boolean logic
\begin{itemize}
\item Example: $A\Rightarrow B+C\vdash(A\Rightarrow B)+(A\Rightarrow C)$
does not hold in IPL
\item This is counter-intuitive!
\item We cannot implement a function with this type:
\end{itemize}
\begin{lyxcode}
\textcolor{blue}{\footnotesize{}def~q{[}A,B,C{]}(f:~A~$\Rightarrow$~Either{[}B,~C{]}):~Either{[}A~$\Rightarrow$~B,~A~$\Rightarrow$~C{]}}{\footnotesize \par}
\end{lyxcode}
\begin{itemize}
\item Disjunction is ``constructive'': need to supply one of the parts
\begin{itemize}
\item But \texttt{\textcolor{blue}{\footnotesize{}Either{[}A $\Rightarrow$
B, A $\Rightarrow$ C{]}}} is not a function of \texttt{\textcolor{blue}{\footnotesize{}A}} 
\end{itemize}
\end{itemize}
\item Implication works somewhat differently
\begin{itemize}
\item Example: $\left(\left(A\Rightarrow B\right)\Rightarrow A\right)\Rightarrow A$
holds in Boolean logic but not in IPL
\item Cannot compute an \texttt{\textcolor{blue}{\footnotesize{}x:\ A}}
because of insufficient data
\end{itemize}
\item Conjunction works the same as in Boolean logic
\begin{itemize}
\item Example: 
\[
A\Rightarrow B\times C\vdash\left(A\Rightarrow B\right)\times\left(A\Rightarrow C\right)
\]
 
\end{itemize}
\end{itemize}
\end{frame}

\begin{frame}{The logic of types III}


\framesubtitle{How to determine whether a given IPL formula is a theorem?}
\begin{itemize}
\item The IPL cannot have a truth table with a fixed number of truth values
\begin{itemize}
\item This was shown by G\"odel in 1932 (see \href{https://en.wikipedia.org/wiki/Many-valued_logic}{Wikipedia page})
\end{itemize}
\item The IPL has a decision procedure (algorithm) that either finds a proof
for a given IPL formula, or determines that there is no proof
\item There may be several inequivalent proofs of an IPL theorem
\item Each proof can be \emph{automatically translated} into code
\begin{itemize}
\item The \href{https://github.com/Chymyst/curryhoward}{curryhoward} library
implements an IPL prover as a Scala macro, and generates Scala code
from types
\item The \href{https://hackage.haskell.org/package/djinn-ghc}{djinn-ghc}
compiler plugin and the \href{https://github.com/nomeata/ghc-justdoit}{JustDoIt plugin}
implement an IPL prover in Haskell, and generate Haskell code from
types
\end{itemize}
\item All these IPL provers use the same basic algorithm called LJT 
\begin{itemize}
\item and all cite the same paper {\footnotesize{}\href{https://rd.host.cs.st-andrews.ac.uk/publications/jsl57.pdf}{[Dyckhoff 1992]}}{\footnotesize \par}
\item because most other papers on this subject are incomprehensible to
non-specialists, or describe algorithms that are too complicated
\end{itemize}
\end{itemize}
\end{frame}

\begin{frame}{Proof search I: looking for an algorithm}


\framesubtitle{Why our initial presentation of IPL does not give a proof search
algorithm}

The FP type constructions give nine axioms and three derivation rules:

\begin{minipage}[t]{0.49\columnwidth}%
\begin{itemize}
\item $\Gamma,A,B\vdash A\times B$ 
\item $\Gamma,A\times B\vdash A$ 
\item $\Gamma,A\times B\vdash B$
\item $\Gamma,A\Rightarrow B,A\vdash B$
\item $\Gamma,A\vdash A+B$ 
\item $\Gamma,B\vdash A+B$
\item $\Gamma,A+B,A\Rightarrow C,B\Rightarrow C\vdash C$
\item $\Gamma\vdash1$
\item $\Gamma,A\vdash A$
\end{itemize}
%
\end{minipage}%
\begin{minipage}[t]{0.49\columnwidth}%
\[
\frac{\Gamma,A\vdash B}{\Gamma\vdash A\Rightarrow B}
\]
\[
\frac{\Gamma\vdash G}{\Gamma,D\vdash G}
\]
\[
\frac{\Gamma,A,B\vdash G}{\Gamma,B,A\vdash G}
\]
%
\end{minipage}

\medskip{}
Can we use these rules to obtain a finite and complete search tree?
No.
\begin{itemize}
\item Try proving $A,B+C\vdash A\times B+C$: cannot find matching rules
\begin{itemize}
\item Need a better formulation of the logic
\end{itemize}
\end{itemize}
\end{frame}

\begin{frame}{Proof search II: Gentzen's calculus LJ (1935)}

\begin{itemize}
\item A ``complete and sound calculus'' is a set of axioms and derivation
rules that will yield all (and only!) theorems of the logic
\begin{align*}
\text{(}X\text{ is atomic)\,}\frac{}{\Gamma,{\color{blue}X}\vdash X}\:Id & \qquad\frac{}{\Gamma\vdash{\color{blue}\top}}\,\top\\
\frac{\Gamma,A\Rightarrow B\vdash A\quad\;\Gamma,B\vdash C}{\Gamma,{\color{blue}A\Rightarrow B}\vdash C}\:L\Rightarrow & \qquad\frac{\Gamma,A\vdash B}{\Gamma\vdash{\color{blue}A\Rightarrow B}}\,R\Rightarrow\\
\frac{\Gamma,A\vdash C\quad\;\Gamma,B\vdash C}{\Gamma,{\color{blue}A+B}\vdash C}\:L+ & \qquad\frac{\Gamma\vdash A_{i}}{\Gamma\vdash{\color{blue}A_{1}+A_{2}}}\,R+_{i}\\
\frac{\Gamma,A_{i}\vdash C}{\Gamma,{\color{blue}A_{1}\times A_{2}}\vdash C}\:L\times_{i} & \qquad\frac{\Gamma\vdash A\quad\;\Gamma\vdash B}{\Gamma\vdash{\color{blue}A\times B}}\,R\times
\end{align*}
\item Two axioms and eight derivation rules
\begin{itemize}
\item Each derivation rule says: The sequent at bottom will be proved if
proofs are given for sequent(s) at top
\end{itemize}
\item Use these rules ``bottom-up'' to perform a proof search
\begin{itemize}
\item Sequents are nodes and proofs are edges in the proof search tree
\end{itemize}
\end{itemize}
\end{frame}

\begin{frame}{Proof search example I}

Example: to prove $\left(\left(R\Rightarrow R\right)\Rightarrow Q\right)\Rightarrow Q$
\begin{itemize}
\item Root sequent $S_{0}:\emptyset\vdash\left(\left(R\Rightarrow R\right)\Rightarrow Q\right)\Rightarrow Q$
\item $S_{0}$ with rule $R\Rightarrow$ yields $S_{1}:\left(R\Rightarrow R\right)\Rightarrow Q\vdash Q$
\item $S_{1}$ with rule $L\Rightarrow$ yields $S_{2}:\left(R\Rightarrow R\right)\Rightarrow Q\vdash R\Rightarrow R$
and $S_{3}:Q\vdash Q$
\item Sequent $S_{3}$ follows from the $Id$ axiom; it remains to prove
$S_{2}$
\item $S_{2}$ with rule $L\Rightarrow$ yields $S_{4}:\left(R\Rightarrow R\right)\Rightarrow Q\vdash R\Rightarrow R$
and $S_{5}:Q\vdash R\Rightarrow R$
\begin{itemize}
\item We are stuck here because $S_{4}=S_{2}$ (we are in a loop)
\item We can prove $S_{5}$, but that will not help
\item So we backtrack (erase $S_{4}$, $S_{5}$) and apply another rule
to $S_{2}$
\end{itemize}
\item $S_{2}$ with rule $R\Rightarrow$ yields $S_{6}:\left(R\Rightarrow R\right)\Rightarrow Q;R\vdash R$
\item Sequent $S_{6}$ follows from the $Id$ axiom
\end{itemize}
Therefore we have proved $S_{0}$

Since $\left(\left(R\Rightarrow R\right)\Rightarrow Q\right)\Rightarrow Q$
is derived from no premises, it is a theorem

$Q.E.D.$
\end{frame}

\begin{frame}{Proof search III: The calculus LJT}


\framesubtitle{Vorobieff-Hudelmaier-Dyckhoff, 1950-1990}
\begin{itemize}
\item The Gentzen calculus LJ will loop if rule $L\Rightarrow$ is applied
$\geq2$ times
\item The calculus LJT keeps all rules of LJ except rule $L\Rightarrow$
\item Replace rule $L\Rightarrow$ by pattern-matching on $A$ in the premise
$A\Rightarrow B$:
\begin{align*}
\text{(}X\text{ is atomic)\,}\frac{\Gamma,X,B\vdash D}{\Gamma,X,{\color{blue}X\Rightarrow B}\vdash D}\:L\Rightarrow_{1}\\
\frac{\Gamma,A\Rightarrow B\Rightarrow C\vdash D}{\Gamma,{\color{blue}(A\times B)\Rightarrow C}\vdash D}\:L\Rightarrow_{2}\\
\frac{\Gamma,A\Rightarrow C,B\Rightarrow C\vdash D}{\Gamma,{\color{blue}(A+B)\Rightarrow C}\vdash D}\:L\Rightarrow_{3}\\
\frac{\Gamma,B\Rightarrow C\vdash A\Rightarrow B\quad\quad\Gamma,C\vdash D}{\Gamma,{\color{blue}(A\Rightarrow B)\Rightarrow C}\vdash D}\:L\Rightarrow_{4}
\end{align*}
\item When using LJT rules, the proof tree has no loops and terminates
\begin{itemize}
\item See \href{http://citeseer.ist.psu.edu/viewdoc/summary?doi=10.1.1.35.2618}{this paper}
for an explicit decreasing measure on the proof tree
\end{itemize}
\end{itemize}
\end{frame}

\begin{frame}{Proof search IV: The calculus LJT}


\framesubtitle{``\emph{It is obvious that it is obvious}'' \textendash{} a mathematician
after thinking for a half-hour}
\begin{itemize}
\item Rule $L\Rightarrow_{4}$ is based on the key theorem: {\footnotesize{}
\[
\left(\left(A\Rightarrow B\right)\Rightarrow C\right)\Rightarrow\left(A\Rightarrow B\right)\,\Longleftrightarrow\,\left(B\Rightarrow C\right)\Rightarrow\left(A\Rightarrow B\right)
\]
}{\footnotesize \par}
\item The key theorem for rule $L\Rightarrow_{4}$ is attributed to Vorobieff
(1958):
\end{itemize}
\begin{center}
\includegraphics[width=0.8\textwidth]{0_Users_sergei_winitzki_Code_talks_ftt-fp_Vorobieff-lemma.png}
\par\end{center}

\begin{center}
{\footnotesize{}{[}R. Dyckhoff, }\emph{\footnotesize{}Contraction-Free
Sequent Calculi for Intuitionistic Logic}{\footnotesize{}, 1992{]}}
\par\end{center}{\footnotesize \par}
\begin{itemize}
\item A stepping stone to this theorem:{\footnotesize{}
\[
\left(\left(A\Rightarrow B\right)\Rightarrow C\right)\Rightarrow B\Rightarrow C
\]
}Proof (\emph{obviously} trivial): $f^{\left(A\Rightarrow B\right)\Rightarrow C}\Rightarrow b^{B}\Rightarrow f\:(x^{A}\Rightarrow b)$
\begin{itemize}
\item \emph{Details are left as exercise for the reader}
\end{itemize}
\end{itemize}
\end{frame}

\begin{frame}{Proof search V: From deduction rules to code}

\begin{itemize}
\item The new rules are equivalent to the old rules, therefore...
\begin{itemize}
\item Proof of a sequent $A,B,C\vdash G$ $\Leftrightarrow$ code/expression
$t(a,b,c):G$
\item Also can be seen as a function $t$ from $A,B,C$ to $G$
\end{itemize}
\item Sequent in a proof follows from an axiom or from a transforming rule
\begin{itemize}
\item The two axioms are fixed expressions, $x^{A}\Rightarrow x$ and $1$
\item Each rule has a \emph{proof transformer} function: $\text{PT}_{R\Rightarrow}$
, $\text{PT}_{L+}$ , etc.
\end{itemize}
\item Examples of proof transformer functions:
\begin{align*}
\frac{\Gamma,A\vdash C\quad\;\Gamma,B\vdash C}{\Gamma,{\color{blue}A+B}\vdash C}\:L+\\
PT_{L+}(t_{1}^{A\Rightarrow C},t_{2}^{B\Rightarrow C})=x^{A+B}\Rightarrow & \ x\ \text{match}\begin{cases}
a^{A}\Rightarrow t_{1}(a)\\
b^{B}\Rightarrow t_{2}(b)
\end{cases}
\end{align*}
\begin{align*}
\frac{\Gamma,A\Rightarrow B\Rightarrow C\vdash D}{\Gamma,{\color{blue}(A\times B)\Rightarrow C}\vdash D}\:L\Rightarrow_{2}\\
PT_{L\Rightarrow_{2}}(f^{\left(A\Rightarrow B\Rightarrow C\right)\Rightarrow D})=g^{A\times B\Rightarrow C}\Rightarrow & f\,(x^{A}\Rightarrow y^{B}\Rightarrow g(x,y))
\end{align*}
\item Verify that we can indeed produce PTs for every rule of LJT
\end{itemize}
\end{frame}

\begin{frame}{Proof search example II: deriving code}

Once a proof tree is found, start from leaves and apply PTs
\begin{itemize}
\item For each sequent $S_{i}$, this will derive a \textbf{proof expression}
$t_{i}$
\item Example: to prove $S_{0}$, start from $S_{6}$ backwards:{\footnotesize{}
\begin{align*}
S_{6}:\left(R\Rightarrow R\right)\Rightarrow Q;R\vdash R\quad(\text{axiom }Id)\quad & t_{6}(rrq,r)=r\\
S_{2}:\left(R\Rightarrow R\right)\Rightarrow Q\vdash\left(R\Rightarrow R\right)\quad\text{PT}_{R\Rightarrow}(t_{6})\quad & t_{2}(rrq)=\left(r\Rightarrow t_{6}(rrq,r)\right)\\
S_{3}:Q\vdash Q\quad(\text{axiom }Id)\quad & t_{3}(q)=q\\
S_{1}:\left(R\Rightarrow R\right)\Rightarrow Q\vdash Q\quad\text{PT}_{L\Rightarrow}(t_{2},t_{3})\quad & t_{1}(rrq)=t_{3}(rrq(t_{2}(rrq)))\\
S_{0}:\emptyset\vdash\left(\left(R\Rightarrow R\right)\Rightarrow Q\right)\Rightarrow Q\quad\text{PT}_{R\Rightarrow}(t_{1})\quad & t_{0}=\left(rrq\Rightarrow t_{1}(rrq)\right)
\end{align*}
}{\footnotesize \par}
\item The proof expression for $S_{0}$ is then obtained as
\begin{align*}
t_{0} & =rrq\Rightarrow t_{3}\left(rrq\left(t_{2}\left(rrq\right)\right)\right)=rrq\Rightarrow rrq(r\Rightarrow t_{6}\left(rrq,r\right)\\
 & =rrq\Rightarrow rrq\left(r\Rightarrow r\right)
\end{align*}
Simplified final code having the required type: 
\[
t_{0}:\left(\left(R\Rightarrow R\right)\Rightarrow Q\right)\Rightarrow Q=\left(rrq\Rightarrow rrq\left(r\Rightarrow r\right)\right)
\]
\end{itemize}
\end{frame}

\begin{frame}{Type isomorphisms I: identities}


\framesubtitle{Using known properties of propositional logic and arithmetic}

Are $A+B,\:A\times B$ more like logic $\left(A\vee B,\;A\wedge B\right)$
or like arithmetic?
\begin{itemize}
\item Some identities in logic ($\forall A\forall B\forall C$ is assumed)
written using $\times$, $+$:
\begin{align*}
A\times1=A; & \quad A\times B=B\times A\\
A+1=1; & \quad A+B=B+A\\
(A\times B)\times C=A\times(B\times C); & \quad A+(B\times C)=(A+B)\times(A+C)\\
(A+B)+C=A+(B+C); & \quad A\times(B+C)=(A\times B)+(A\times C)\\
(A\times B)\Rightarrow C & =A\Rightarrow(B\Rightarrow C)\\
A\Rightarrow(B\times C) & =(A\Rightarrow B)\times(A\Rightarrow C)\\
(A+B)\Rightarrow C & =(A\Rightarrow C)\times(B\Rightarrow C)
\end{align*}
\item Each identity means 2 function types: $X=Y$ is $X\Rightarrow Y\text{ \emph{and} }Y\Rightarrow X$ 
\begin{itemize}
\item These functions exist and convert values between types $X$ and $Y$
\item Do these functions express \emph{equivalence} of the types $X$ and
$Y$?
\end{itemize}
\end{itemize}
\end{frame}

\begin{frame}{Type isomorphisms II}

\begin{itemize}
\item Types $A$ and $B$ are isomorphic, $A\equiv B$, if there is a 1-to-1
correspondence between the sets of values of these types
\begin{itemize}
\item Need to find two functions $f:A\Rightarrow B$ and $g:B\Rightarrow A$
such that $f\circ g=id$ and $g\circ f=id$
\end{itemize}
\end{itemize}
Example 1: Is $\forall A:A\times1\equiv A$? Types in Scala: \texttt{\textcolor{blue}{\footnotesize{}(A,
Unit)}} and \texttt{\textcolor{blue}{\footnotesize{}A}}{\footnotesize \par}
\begin{itemize}
\item Two functions with types $\forall A:A\times1\Rightarrow A$ and $\forall A:A\Rightarrow A\times1$:
\end{itemize}
\begin{lyxcode}
\textcolor{blue}{\footnotesize{}def~f1{[}A{]}(pair:~(A,~Unit)):~A~=~pair.\_1}{\footnotesize \par}

\textcolor{blue}{\footnotesize{}def~f2{[}A{]}(x:~A):~(A,~Unit)~=~(x,~())}{\footnotesize \par}
\end{lyxcode}
\begin{itemize}
\item Verify that both their compositions equal \texttt{\textcolor{blue}{\footnotesize{}identity}} 
\end{itemize}
Example 2: Is $\forall A:1+A\equiv1$? (The formula $\forall A:A\vee1=1$
is a theorem!)
\begin{itemize}
\item Types in Scala: \texttt{\textcolor{blue}{\footnotesize{}Option{[}A{]}}}
and \texttt{\textcolor{blue}{\footnotesize{}Unit}} 
\begin{itemize}
\item These types are obviously \emph{not} equivalent
\end{itemize}
\end{itemize}
\emph{Some} logic identities yield\emph{ }isomorphisms of types
\begin{itemize}
\item Which ones \emph{do} \emph{not} yield isomorphisms, and why?
\end{itemize}
\end{frame}

\begin{frame}{Type isomorphisms III}


\framesubtitle{Verifying type equivalence by implementing isomorphisms}
\begin{itemize}
\item Need to verify that $f_{1}\circ f_{2}=id$ and $f_{2}\circ f_{1}=id$
\end{itemize}
Example 3: $\forall A\forall B\forall C:(A\times B)\times C\equiv A\times(B\times C)$
\begin{lyxcode}
\textcolor{blue}{\footnotesize{}def~f1{[}A,B,C{]}:~(((A,~B),~C))~$\Rightarrow$~(A,~(B,~C))~=~???}{\footnotesize \par}

\textcolor{blue}{\footnotesize{}def~f2{[}A,B,C{]}:~((A,~(B,~C)))~$\Rightarrow$~((A,~B),~C)~=~???}{\footnotesize \par}
\end{lyxcode}
Example 4: $\forall A\forall B\forall C:(A+B)\times C\equiv A\times C+B\times C$
\begin{lyxcode}
\textcolor{blue}{\footnotesize{}def~f1{[}A,B,C{]}:~((Either{[}A,B{]},~C))~$\Rightarrow$~Either{[}(A,C),~(B,C){]}~=~???}{\footnotesize \par}

\textcolor{blue}{\footnotesize{}def~f2{[}A,B,C{]}:~Either{[}(A,C),~(B,C){]}~$\Rightarrow$~(Either{[}A,~B{]},~C)~=~???}{\footnotesize \par}
\end{lyxcode}
Example 5: $\forall A\forall B\forall C:(A+B)\Rightarrow C\equiv(A\Rightarrow C)\times(B\Rightarrow C)$
\begin{lyxcode}
\textcolor{blue}{\footnotesize{}def~f1{[}A,B,C{]}:~(Either{[}A,~B{]}~$\Rightarrow$~C)~$\Rightarrow$~(A~$\Rightarrow$~C,~B~$\Rightarrow$~C)~=~???}{\footnotesize \par}

\textcolor{blue}{\footnotesize{}def~f2{[}A,B,C{]}:~((A~$\Rightarrow$~C,~B~$\Rightarrow$~C))~$\Rightarrow$~Either{[}A,~B{]}~$\Rightarrow$~C~=~???}{\footnotesize \par}
\end{lyxcode}
Example 6: $\forall A\forall B\forall C:A+B\times C\not\equiv(A+B)\times(A+C)$
\textendash{} ``information loss''
\begin{lyxcode}
\textcolor{blue}{\footnotesize{}def~f1{[}A,B,C{]}:~Either{[}A,(B,C){]}$\Rightarrow$(Either{[}A,B{]},Either{[}A,C{]})~=~???}{\footnotesize \par}

\textcolor{blue}{\footnotesize{}def~f2{[}A,B,C{]}:~((Either{[}A,B{]},Either{[}A,C{]}))~$\Rightarrow$~Either{[}A,(B,C){]}~=~???}{\footnotesize \par}
\end{lyxcode}
\end{frame}

\begin{frame}{Type isomorphisms IV}


\framesubtitle{Logical CH vs.\ arithmetical CH}
\begin{itemize}
\item WLOG consider types $A,B,...$ that have \emph{finite} sets of possible
values
\begin{itemize}
\item Sum type $A+B$ (size $\left|A\right|+\left|B\right|$) provides a
disjoint union of sets
\item Product type $A\times B$ (size $\left|A\right|\cdot\left|B\right|$)
provides a Cartesian product of sets
\begin{itemize}
\item Have identities $\left(a+b\right)+c=a+\left(b+c\right)$, $\left(a\times b\right)\times c=a\times(b\times c)$,
$1\times a=a$, $\left(a+b\right)\times c=a\times c+b\times c$, ...
\textendash{} as in ``school-level'' algebra
\end{itemize}
\item Function type $A\Rightarrow B$ provides the set of all maps between
sets
\begin{itemize}
\item The size of $A\Rightarrow B$ is $\left|B\right|^{\left|A\right|}$
\item Have identities $a^{c}\times b^{c}=\left(a\times b\right)^{c}$, $a^{b+c}=a^{b}\times a^{c}$,
$a^{b\times c}=\left(a^{b}\right)^{c}$
\end{itemize}
\end{itemize}
\item If the set size (\textbf{cardinality}) differs, $A$ and $B$ cannot
be equivalent 
\end{itemize}
The meaning of the type/logic/arithmetic correspondence:
\begin{itemize}
\item Arithmetical identities signify type equivalence (isomorphism)
\item Logic identities only signify \emph{equal implementability} of types
\end{itemize}
Reasoning about types is \emph{school-level algebra} with polynomials
and powers
\begin{itemize}
\item \textbf{Exp-polynomial }expressions: constants, sums, products, exponentials
\begin{itemize}
\item exp-poly types: primitive types, disjunctions, tuples, functions
\item polynomial types are commonly called ``algebraic types''
\end{itemize}
\end{itemize}
\end{frame}

\begin{frame}{Making practical use of the CH correspondence I}


\framesubtitle{Implications for actually writing code}

What can we do now?
\begin{itemize}
\item Given a fully parametric type, decide whether it can be implemented
in code (``type is inhabited''e computer \emph{generate} the code from type when possible
\begin{itemize}
\item This is often (not always) possible for fully type-parametric functions
\end{itemize}
\item Decide type isomorphisms using the ``arithmetical CH''
\item Isomorphically transform types using school-level algebra
\end{itemize}
What problems cannot be solved with these tools?
\begin{itemize}
\item Automatically generate code satisfying properties (e.g.\ isomorphism) 
\item Express complicated conditions via types (e.g.\ ``array is sorted'') 
\item Generate code using type constructors with properties (e.g.\ \texttt{\textcolor{blue}{\footnotesize{}map}})
\begin{itemize}
\item Scala type signature: \texttt{\textcolor{blue}{\footnotesize{}(x:\ List{[}A{]}).map{[}B{]}(f:\ A
$\Rightarrow$ B):\ List{[}B{]}}}{\footnotesize \par}
\item This formula has a quantifier \emph{inside}: $\text{List}^{A}\Rightarrow(\forall B:f^{A\Rightarrow B}\Rightarrow\text{List}^{B})$
\item This requires \textbf{first-order logic}, which is generally \emph{undecidable}
(no algorithm can guarantee finding a proof or showing its absence)
\end{itemize}
\end{itemize}
\end{frame}

\begin{frame}{Some caveats}

\begin{itemize}
\item The CH correspondence becomes informative only with parameterized
types. For concrete types, e.g.\ \texttt{\textcolor{blue}{\footnotesize{}Int}},
we can always produce \emph{some} value even with no previous data,
so $\mathcal{CH}(\text{Int})$ is always true.
\item Functions such as \texttt{\textcolor{blue}{\footnotesize{}(x:\ Int)
$\Rightarrow$ x + 1}} have type \texttt{\textcolor{blue}{\footnotesize{}Int}}
$\Rightarrow$\texttt{\textcolor{blue}{\footnotesize{} Int}}, and
the type signature is insufficient to specify the code. Only for fully
type-parametric functions the type signature can be, in some cases,
informative enough for deriving the code automatically.
\item Having an arithmetic identity does not \emph{guarantee} that we have
a type equivalence via CH (it is a necessary but not a sufficient
condition); but it does yield a type equivalence in all cases I looked
at so far.
\item Scala's type \texttt{\textcolor{blue}{\footnotesize{}Nothing}} and
Haskell's type \texttt{\textcolor{blue}{\footnotesize{}Void}} correspond
to the logical constant $False$; but the practical uses of $False$
are extremely limited. 
\item We did not talk about the logical negation because it is defined as
$\neg A\equiv A\Rightarrow False$ and its practical use is as limited
as that of $False$.
\end{itemize}
\end{frame}

\begin{frame}{Making practical use of the CH correspondence II}


\framesubtitle{Implications for designing new programming languages}
\begin{itemize}
\item The CH correspondence maps the type system of each programming language
into a certain system of logical propositions 
\item Scala, Haskell, OCaml, F\#, Swift, Rust, etc.~are mapped into the
full constructive logic (all logical operations are available)
\begin{itemize}
\item C, C++, Java, C\#, etc.~are mapped to \emph{incomplete} \emph{logics}
\textendash{} without ``or'' and without ``true'' / ``false''
\item Python, JavaScript, Ruby, Clojure, etc.~have only one type (``any
value'') and are mapped to logics with only one proposition
\end{itemize}
\item The CH correspondence is a principle for designing type systems:
\begin{itemize}
\item Choose a complete logic, free of inconsistency
\begin{itemize}
\item Mathematicians have studied all kinds of logics and determined which
ones are interesting, and found the minimal sets of axioms for them
\item Modal logic, temporal logic, linear logic, etc.
\end{itemize}
\item Provide easy type constructions for basic operations (e.g.~``\emph{or}'',
``\emph{and}'')
\begin{itemize}
\item There should be a type for every logical formula and vice versa
\item There should be a code construct for each rule of the logic
\end{itemize}
\end{itemize}
\end{itemize}
\end{frame}

\end{document}
